<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>Table of contents</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>
</head>

<body><script>
$( function() {
    var icons = {
      header: "ui-icon-circle-arrow-e",
      activeHeader: "ui-icon-circle-arrow-s"
    };

    $("#accordion").accordion({
      collapsible : true,
      active : false,
      icons : icons,
      heightStyle : 'content'
    });

    // Enable navigation links in section headers
    $('#accordion').each(function() {
      this.addEventListener('click', ev => {
        if ($(ev.target).closest('a').length > 0) ev.stopPropagation();
      }, {capture: true});
    });
  } );
</script>


<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 1: Logical Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>
</div>

<div id="main">

<div id="toc">
<div id="accordion">
<h2><a href="Preface.html">Preface</a></h2>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab1">Welcome</a>

</li>
<li><a href="Preface.html#lab2">Overview</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab3">Logic</a>

</li>
<li><a href="Preface.html#lab4">Proof Assistants</a>

</li>
<li><a href="Preface.html#lab5">Functional Programming</a>

</li>
<li><a href="Preface.html#lab6">Further Reading</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab7">Practicalities</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab8">System Requirements</a>

</li>
<li><a href="Preface.html#lab9">Exercises</a>

</li>
<li><a href="Preface.html#lab10">Downloading the Coq Files</a>

</li>
<li><a href="Preface.html#lab11">Chapter Dependencies</a>

</li>
<li><a href="Preface.html#lab12">Recommended Citation Format</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab13">Resources</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab14">Sample Exams</a>

</li>
<li><a href="Preface.html#lab15">Lecture Videos</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab16">Note for Instructors</a>

</li>
<li><a href="Preface.html#lab17">Translations</a>

</li>
<li><a href="Preface.html#lab18">Thanks</a>

</li>
</ul>
</div>
<h2><a href="Basics.html">Functional Programming in Coq &nbsp;&nbsp; (<i>Basics</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Basics.html#lab19">Introduction</a>

</li>
<li><a href="Basics.html#lab20">Data and Functions</a>
<div>
<ul class="doclist">
<li><a href="Basics.html#lab21">Enumerated Types</a>

</li>
<li><a href="Basics.html#lab22">Days of the Week</a>

</li>
<li><a href="Basics.html#lab23">Homework Submission Guidelines</a>

</li>
<li><a href="Basics.html#lab24">Booleans</a>

</li>
<li><a href="Basics.html#lab27">Types</a>

</li>
<li><a href="Basics.html#lab28">New Types from Old</a>

</li>
<li><a href="Basics.html#lab29">Modules</a>

</li>
<li><a href="Basics.html#lab30">Tuples</a>

</li>
<li><a href="Basics.html#lab31">Numbers</a>

</li>
</ul>
</div>

</li>
<li><a href="Basics.html#lab34">Proof by Simplification</a>

</li>
<li><a href="Basics.html#lab35">Proof by Rewriting</a>

</li>
<li><a href="Basics.html#lab38">Proof by Case Analysis</a>
<div>
<ul class="doclist">
<li><a href="Basics.html#lab41">More on Notation (Optional)</a>

</li>
<li><a href="Basics.html#lab42">Fixpoints and Structural Recursion (Optional)</a>

</li>
</ul>
</div>

</li>
<li><a href="Basics.html#lab44">More Exercises</a>

</li>
<li><a href="Basics.html#lab49">Testing Your Solutions</a>

</li>
</ul>
</div>
<h2><a href="Induction.html">Proof by Induction &nbsp;&nbsp; (<i>Induction</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Induction.html#lab50">Proof by Induction</a>

</li>
<li><a href="Induction.html#lab55">Proofs Within Proofs</a>

</li>
<li><a href="Induction.html#lab56">Formal vs. Informal Proof</a>

</li>
<li><a href="Induction.html#lab59">More Exercises</a>

</li>
</ul>
</div>
<h2><a href="Lists.html">Working with Structured Data &nbsp;&nbsp; (<i>Lists</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Lists.html#lab66">Pairs of Numbers</a>

</li>
<li><a href="Lists.html#lab69">Lists of Numbers</a>

</li>
<li><a href="Lists.html#lab81">Reasoning About Lists</a>
<div>
<ul class="doclist">
<li><a href="Lists.html#lab82">Induction on Lists</a>

</li>
<li><a href="Lists.html#lab84"><span class="inlinecode"><span class="id" title="keyword">Search</span></span></a>

</li>
<li><a href="Lists.html#lab85">List Exercises, Part 1</a>

</li>
<li><a href="Lists.html#lab88">List Exercises, Part 2</a>

</li>
</ul>
</div>

</li>
<li><a href="Lists.html#lab93">Options</a>

</li>
<li><a href="Lists.html#lab96">Partial Maps</a>

</li>
</ul>
</div>
<h2><a href="Poly.html">Polymorphism and Higher-Order Functions &nbsp;&nbsp; (<i>Poly</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Poly.html#lab101">Polymorphism</a>
<div>
<ul class="doclist">
<li><a href="Poly.html#lab102">Polymorphic Lists</a>

</li>
<li><a href="Poly.html#lab111">Polymorphic Pairs</a>

</li>
<li><a href="Poly.html#lab114">Polymorphic Options</a>

</li>
</ul>
</div>

</li>
<li><a href="Poly.html#lab116">Functions as Data</a>
<div>
<ul class="doclist">
<li><a href="Poly.html#lab117">Higher-Order Functions</a>

</li>
<li><a href="Poly.html#lab118">Filter</a>

</li>
<li><a href="Poly.html#lab119">Anonymous Functions</a>

</li>
<li><a href="Poly.html#lab122">Map</a>

</li>
<li><a href="Poly.html#lab127">Fold</a>

</li>
<li><a href="Poly.html#lab129">Functions That Construct Functions</a>

</li>
</ul>
</div>

</li>
<li><a href="Poly.html#lab130">Additional Exercises</a>

</li>
</ul>
</div>
<h2><a href="Tactics.html">More Basic Tactics &nbsp;&nbsp; (<i>Tactics</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Tactics.html#lab139">The <span class="inlinecode"><span class="id" title="tactic">apply</span></span> Tactic</a>

</li>
<li><a href="Tactics.html#lab143">The <span class="inlinecode"><span class="id" title="tactic">apply</span></span> <span class="inlinecode"><span class="id" title="keyword">with</span></span> Tactic</a>

</li>
<li><a href="Tactics.html#lab145">The <span class="inlinecode"><span class="id" title="tactic">injection</span></span> and <span class="inlinecode"><span class="id" title="tactic">discriminate</span></span> Tactics</a>

</li>
<li><a href="Tactics.html#lab148">Using Tactics on Hypotheses</a>

</li>
<li><a href="Tactics.html#lab149">Varying the Induction Hypothesis</a>

</li>
<li><a href="Tactics.html#lab154">Unfolding Definitions</a>

</li>
<li><a href="Tactics.html#lab155">Using <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> on Compound Expressions</a>

</li>
<li><a href="Tactics.html#lab158">Review</a>

</li>
<li><a href="Tactics.html#lab159">Additional Exercises</a>

</li>
</ul>
</div>
<h2><a href="Logic.html">Logic in Coq &nbsp;&nbsp; (<i>Logic</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Logic.html#lab166">Logical Connectives</a>
<div>
<ul class="doclist">
<li><a href="Logic.html#lab167">Conjunction</a>

</li>
<li><a href="Logic.html#lab171">Disjunction</a>

</li>
<li><a href="Logic.html#lab174">Falsehood and Negation</a>

</li>
<li><a href="Logic.html#lab180">Truth</a>

</li>
<li><a href="Logic.html#lab181">Logical Equivalence</a>

</li>
<li><a href="Logic.html#lab184">Setoids and Logical Equivalence</a>

</li>
<li><a href="Logic.html#lab185">Existential Quantification</a>

</li>
</ul>
</div>

</li>
<li><a href="Logic.html#lab188">Programming with Propositions</a>

</li>
<li><a href="Logic.html#lab193">Applying Theorems to Arguments</a>

</li>
<li><a href="Logic.html#lab194">Coq vs. Set Theory</a>
<div>
<ul class="doclist">
<li><a href="Logic.html#lab195">Functional Extensionality</a>

</li>
<li><a href="Logic.html#lab197">Propositions vs. Booleans</a>

</li>
<li><a href="Logic.html#lab203">Classical vs. Constructive Logic</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="IndProp.html">Inductively Defined Propositions &nbsp;&nbsp; (<i>IndProp</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab207">Inductively Defined Propositions</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab208">Inductive Definition of Evenness</a>

</li>
</ul>
</div>

</li>
<li><a href="IndProp.html#lab210">Using Evidence in Proofs</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab211">Inversion on Evidence</a>

</li>
<li><a href="IndProp.html#lab214">Induction on Evidence</a>

</li>
</ul>
</div>

</li>
<li><a href="IndProp.html#lab219">Inductive Relations</a>

</li>
<li><a href="IndProp.html#lab228">Case Study: Regular Expressions</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab232">The <span class="inlinecode"><span class="id" title="var">remember</span></span> Tactic</a>

</li>
</ul>
</div>

</li>
<li><a href="IndProp.html#lab236">Case Study: Improving Reflection</a>

</li>
<li><a href="IndProp.html#lab239">Additional Exercises</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab247">Extended Exercise: A Verified Regular-Expression Matcher</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Maps.html">Total and Partial Maps &nbsp;&nbsp; (<i>Maps</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Maps.html#lab256">The Coq Standard Library</a>

</li>
<li><a href="Maps.html#lab257">Identifiers</a>

</li>
<li><a href="Maps.html#lab258">Total Maps</a>

</li>
<li><a href="Maps.html#lab266">Partial maps</a>

</li>
</ul>
</div>
<h2><a href="ProofObjects.html">The Curry-Howard Correspondence &nbsp;&nbsp; (<i>ProofObjects</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="ProofObjects.html#lab267">Proof Scripts</a>

</li>
<li><a href="ProofObjects.html#lab269">Quantifiers, Implications, Functions</a>

</li>
<li><a href="ProofObjects.html#lab270">Programming with Tactics</a>

</li>
<li><a href="ProofObjects.html#lab271">Logical Connectives as Inductive Types</a>
<div>
<ul class="doclist">
<li><a href="ProofObjects.html#lab272">Conjunction</a>

</li>
<li><a href="ProofObjects.html#lab274">Disjunction</a>

</li>
<li><a href="ProofObjects.html#lab276">Existential Quantification</a>

</li>
<li><a href="ProofObjects.html#lab278"><span class="inlinecode"><span class="id" title="var">True</span></span> and <span class="inlinecode"><span class="id" title="var">False</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="ProofObjects.html#lab281">Equality</a>
<div>
<ul class="doclist">
<li><a href="ProofObjects.html#lab284">Inversion, Again</a>

</li>
</ul>
</div>

</li>
<li><a href="ProofObjects.html#lab285">The Coq Trusted Computing Base</a>

</li>
</ul>
</div>
<h2><a href="IndPrinciples.html">Induction Principles &nbsp;&nbsp; (<i>IndPrinciples</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="IndPrinciples.html#lab286">Basics</a>

</li>
<li><a href="IndPrinciples.html#lab291">Polymorphism</a>

</li>
<li><a href="IndPrinciples.html#lab296">Induction Hypotheses</a>

</li>
<li><a href="IndPrinciples.html#lab297">More on the <span class="inlinecode"><span class="id" title="tactic">induction</span></span> Tactic</a>

</li>
<li><a href="IndPrinciples.html#lab299">Induction Principles for Propositions</a>

</li>
<li><a href="IndPrinciples.html#lab300">Another Form of Induction Principles on Propositions (Optional)</a>

</li>
<li><a href="IndPrinciples.html#lab301">Formal vs. Informal Proofs by Induction</a>
<div>
<ul class="doclist">
<li><a href="IndPrinciples.html#lab302">Induction Over an Inductively Defined Set</a>

</li>
<li><a href="IndPrinciples.html#lab303">Induction Over an Inductively Defined Proposition</a>

</li>
</ul>
</div>

</li>
<li><a href="IndPrinciples.html#lab304">Explicit Proof Objects for Induction (Optional)</a>

</li>
</ul>
</div>
<h2><a href="Rel.html">Properties of Relations &nbsp;&nbsp; (<i>Rel</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Rel.html#lab305">Relations</a>

</li>
<li><a href="Rel.html#lab306">Basic Properties</a>

</li>
<li><a href="Rel.html#lab323">Reflexive, Transitive Closure</a>

</li>
</ul>
</div>
<h2><a href="Imp.html">Simple Imperative Programs &nbsp;&nbsp; (<i>Imp</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab326">Arithmetic and Boolean Expressions</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab327">Syntax</a>

</li>
<li><a href="Imp.html#lab328">Evaluation</a>

</li>
<li><a href="Imp.html#lab329">Optimization</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab330">Coq Automation</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab331">Tacticals</a>

</li>
<li><a href="Imp.html#lab338">Defining New Tactic Notations</a>

</li>
<li><a href="Imp.html#lab339">The <span class="inlinecode"><span class="id" title="tactic">omega</span></span> Tactic</a>

</li>
<li><a href="Imp.html#lab340">A Few More Handy Tactics</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab341">Evaluation as a Relation</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab342">Inference Rule Notation</a>

</li>
<li><a href="Imp.html#lab344">Equivalence of the Definitions</a>

</li>
<li><a href="Imp.html#lab346">Computational vs. Relational Definitions</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab347">Expressions With Variables</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab348">States</a>

</li>
<li><a href="Imp.html#lab349">Syntax</a>

</li>
<li><a href="Imp.html#lab350">Notations</a>

</li>
<li><a href="Imp.html#lab351">Evaluation</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab352">Commands</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab353">Syntax</a>

</li>
<li><a href="Imp.html#lab354">Desugaring notations</a>

</li>
<li><a href="Imp.html#lab355">The <span class="inlinecode"><span class="id" title="keyword">Locate</span></span> command</a>

</li>
<li><a href="Imp.html#lab358">More Examples</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab361">Evaluating Commands</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab362">Evaluation as a Function (Failed Attempt)</a>

</li>
<li><a href="Imp.html#lab363">Evaluation as a Relation</a>

</li>
<li><a href="Imp.html#lab367">Determinism of Evaluation</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab368">Reasoning About Imp Programs</a>

</li>
<li><a href="Imp.html#lab373">Additional Exercises</a>

</li>
</ul>
</div>
<h2><a href="ImpParser.html">Lexing and Parsing in Coq &nbsp;&nbsp; (<i>ImpParser</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="ImpParser.html#lab382">Internals</a>
<div>
<ul class="doclist">
<li><a href="ImpParser.html#lab383">Lexical Analysis</a>

</li>
<li><a href="ImpParser.html#lab384">Parsing</a>

</li>
</ul>
</div>

</li>
<li><a href="ImpParser.html#lab388">Examples</a>

</li>
</ul>
</div>
<h2><a href="ImpCEvalFun.html">An Evaluation Function for Imp &nbsp;&nbsp; (<i>ImpCEvalFun</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="ImpCEvalFun.html#lab389">A Broken Evaluator</a>

</li>
<li><a href="ImpCEvalFun.html#lab390">A Step-Indexed Evaluator</a>

</li>
<li><a href="ImpCEvalFun.html#lab393">Relational vs. Step-Indexed Evaluation</a>

</li>
<li><a href="ImpCEvalFun.html#lab396">Determinism of Evaluation Again</a>

</li>
</ul>
</div>
<h2><a href="Extraction.html">Extracting ML from Coq &nbsp;&nbsp; (<i>Extraction</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Extraction.html#lab397">Basic Extraction</a>

</li>
<li><a href="Extraction.html#lab398">Controlling Extraction of Specific Types</a>

</li>
<li><a href="Extraction.html#lab399">A Complete Example</a>

</li>
<li><a href="Extraction.html#lab400">Discussion</a>

</li>
<li><a href="Extraction.html#lab401">Going Further</a>

</li>
</ul>
</div>
<h2><a href="Auto.html">More Automation &nbsp;&nbsp; (<i>Auto</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Auto.html#lab402">The <span class="inlinecode"><span class="id" title="tactic">auto</span></span> Tactic</a>

</li>
<li><a href="Auto.html#lab403">Searching For Hypotheses</a>

</li>
<li><a href="Auto.html#lab404">Tactics <span class="inlinecode"><span class="id" title="tactic">eapply</span></span> and <span class="inlinecode"><span class="id" title="tactic">eauto</span></span></a>

</li>
<li><a href="Auto.html#lab405">Constraints on Existential Variables</a>

</li>
</ul>
</div>
<h2><a href="AltAuto.html">More Automation &nbsp;&nbsp; (<i>AltAuto</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="AltAuto.html#lab406">Coq Automation</a>

</li>
<li><a href="AltAuto.html#lab407">Tacticals</a>
<div>
<ul class="doclist">
<li><a href="AltAuto.html#lab413">A Few More Handy Tactics</a>

</li>
<li><a href="AltAuto.html#lab414">Defining New Tactics</a>

</li>
</ul>
</div>

</li>
<li><a href="AltAuto.html#lab415">Decision Procedures</a>
<div>
<ul class="doclist">
<li><a href="AltAuto.html#lab416">The Omega Tactic</a>

</li>
</ul>
</div>

</li>
<li><a href="AltAuto.html#lab417">Search Tactics</a>
<div>
<ul class="doclist">
<li><a href="AltAuto.html#lab418">The <span class="inlinecode"><span class="id" title="tactic">constructor</span></span> tactic.</a>

</li>
<li><a href="AltAuto.html#lab419">The <span class="inlinecode"><span class="id" title="tactic">auto</span></span> Tactic</a>

</li>
<li><a href="AltAuto.html#lab422">The <span class="inlinecode"><span class="id" title="tactic">eapply</span></span> and <span class="inlinecode"><span class="id" title="tactic">eauto</span></span> variants</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Postscript.html">Postscript</a></h2>
<div>
<ul class="doclist">
<li><a href="Postscript.html#lab423">Looking Back</a>

</li>
<li><a href="Postscript.html#lab424">Looking Forward</a>

</li>
<li><a href="Postscript.html#lab425">Resources</a>

</li>
</ul>
</div>
<h2><a href="Bib.html">Bibliography &nbsp;&nbsp; (<i>Bib</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Bib.html#lab426">Resources cited in this volume</a>

</li>
</ul>
</div>
</div>

</div>

</div>

</div>
</body>
</html>